enrich
   intops
with
   comment: 
5.1.3 Narrowing Primitive Conversions

A narrowing conversion of a signed integer to an integral
type T simply discards all but the n lowest order bits, where n is the
number of bits used to represent type T. In addition to a possible
loss of information about the magnitude of the numeric value, this may
cause the sign of the resulting value to differ from the sign of the
input value. ;

   sorts byte
         comment: from -128 to 127, inclusive, 2^8;;
         short
         comment: from -32768 to 32767, inclusive, 2^16;;
         bint
         comment: from -2147483648 to 2147483647, inclusive, 2^32;;
         long
         comment: from -9223372036854775808 to 9223372036854775807, inclusive, 2^64;;
   constants  0b : byte;
              0s : short;
              0bi : bint;
              0l : long;
   functions  b2i : byte → int;
              b2s : byte → short;
              b2bi : byte → bint;
              s2i : short → int;
              s2b : short → byte;
              s2bi : short → bint;
              bi2i : bint → int;
              bi2b : bint → byte;
              bi2s : bint → short;
              i2b : int → byte;
              i2s : int → short;
              i2bi : int → bint;
              i2l : int → long;
              l2i : long → int;
              ub2i : byte → int;
             comment: interpret byte as unsigned byte.;
              us2i : short → int;
             comment: interpret short as unsigned short.;
   predicates  . ∈byte : int;
               . ∈short : int;
               . ∈bint : int;
               . ∈long : int;
               shortOverflow : int;
              comment: true if an overflow occurs, i.e. NOT ∈short;
   
   variables  by : byte;
              byi : byte;
              byj : byte;
              sho : short;
              shoi : short;
              shoj : short;
              bi : bint;
              bj : bint;
              lo : long;
              loi : long;
              loj : long;
   
   

   

   axioms zero-byte :  ⊦ 0b = i2b(0);
          used for: ls;
          zero-short :  ⊦ 0s = i2s(0);
          used for: ls;
          zero-bint :  ⊦ 0bi = i2bi(0);
          used for: ls;
          zero-long :  ⊦ 0l = i2l(0);
          used for: ls;
          inbyte :  ⊦ i ∈byte ↔ ~128 ≤ i ∧ i ≤ 127;
          inshort :  ⊦ i ∈short ↔ ~32768 ≤ i ∧ i ≤ 32767;
          inbint :  ⊦ i ∈bint ↔ ~2147483648 ≤ i ∧ i ≤ 2147483647;
          inlong :  ⊦ i ∈long ↔ ~(2 ^ 63) ≤ i ∧ i ≤ 2 ^ 63 - 1;
          ibi :  ⊦ i2b(b2i(by)) = by;
          used for: s, ls;
          isi :  ⊦ i2s(s2i(sho)) = sho;
          used for: s, ls;
          ibii :  ⊦ i2bi(bi2i(bi)) = bi;
          used for: s, ls;
          ili :  ⊦ i2l(l2i(lo)) = lo;
          used for: s, ls;
          byte2int-in :  ⊦ b2i(by) ∈byte;
          used for: ls;
          short2int-in :  ⊦ s2i(sho) ∈short;
          used for: ls;
          bint2int-in :  ⊦ bi2i(bi) ∈bint;
          used for: ls;
          long2int-in :  ⊦ l2i(lo) ∈long;
          used for: ls;
          bib-in :  ⊦ i ∈byte → b2i(i2b(i)) = i;
          used for: ls;
          sis-in :  ⊦ i ∈short → s2i(i2s(i)) = i;
          used for: ls;
          biibi-in :  ⊦ i ∈bint → bi2i(i2bi(i)) = i;
          used for: ls;
          lib-in :  ⊦ i ∈long → l2i(i2l(i)) = i;
          used for: ls;
          int2byte-out :  ⊦ ¬ i ∈byte → i2b(i) = i2b(bits2int(lastn(8, int2bits(i))));
          int2short-out :  ⊦ ¬ i ∈short → i2s(i) = i2s(bits2int(lastn(16, int2bits(i))));
          int2bint-out :  ⊦ ¬ i ∈bint → i2bi(i) = i2bi(bits2int(lastn(32, int2bits(i))));
          int2long-out :  ⊦ ¬ i ∈long → i2l(i) = i2l(bits2int(lastn(64, int2bits(i))));
          byte2short :  ⊦ b2s(by) = i2s(b2i(by));
          used for: s, ls;
          byte2bint :  ⊦ b2bi(by) = i2bi(b2i(by));
          used for: s, ls;
          short2byte :  ⊦ s2b(sho) = i2b(s2i(sho));
          used for: s, ls;
          short2bint :  ⊦ s2bi(sho) = i2bi(s2i(sho));
          used for: s, ls;
          unsigned-byte :  ⊦ ub2i(by) = bits2int(false ' + fillsgn(8, int2bits(b2i(by))));
          unsigned-short :  ⊦ us2i(sho) = bits2int(false ' + fillsgn(16, int2bits(s2i(sho))));
          shortOverflow :  ⊦ shortOverflow(i) ↔ ¬ i ∈short;
          used for: s, ls;

   

   
end enrich